package org.tau.workshop2011.semantics

import org.tau.workshop2011.expressions.Type
import org.tau.workshop2011.parsing.AST._
import java.lang.AssertionError

sealed class BoolExpansionAssignmentException(msg: String) extends Exception(msg)

class ConflictingAssignmentsException extends BoolExpansionAssignmentException("An assignment to this boolean expression would lead to conflicting values assigned to the same variable!")

class NoPossibleAssignmentsException extends BoolExpansionAssignmentException("No value can be assigned deterministicly to this boolean expression!")

class NonReversibleBooleanException extends BoolExpansionAssignmentException("No obvious way to assign a value to this Boolean Expression!")

trait BoolExpansion {

  def isConstant: Boolean

  def getConstantValue: Boolean

  def canAssignTrue: Boolean

  def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]]

  def canAssignFalse: Boolean

  def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]]

  final def isFalseConstant: Boolean = isConstant && (getConstantValue == false)

  final def isTrueConstant: Boolean = isConstant && (getConstantValue == true)
}

object BoolExpansion {

  @throws(classOf[ConflictingAssignmentsException])
  def combineAssignments(assignments: Map[ResolvedVariable, Literal[_]]*): Map[ResolvedVariable, Literal[_]] = {
    var accumulate = new scala.collection.mutable.HashMap[ResolvedVariable, Literal[_]]

    for (assignment <- assignments) {
      for ((rv, value) <- assignment) {
        if (!(accumulate contains rv))
          accumulate += rv -> value
        else if (accumulate(rv).value != value.value)
          throw new NonReversibleBooleanException
      }
    }

    Map(accumulate.toList: _*)
  }

  @throws(classOf[BoolExpansionAssignmentException])
  def conjunction(elems: BoolExpansion*): BoolExpansion = {
    for (elem <- elems)
      if (elem.isFalseConstant)
        return new ConstBoolExpansion(false)

    val relevant = elems filter {
      (elem) => !elem.isTrueConstant
    }

    if (relevant.length == 0)
      new ConstBoolExpansion(true)
    else if (relevant.length == 1)
      relevant.head
    else {
      /* We will only be able to assign truth to this conjunction if we can
       * assign truth to all it's values
       */
      for (e <- relevant)
        if (!e.canAssignTrue)
          throw new NoPossibleAssignmentsException

      new BoolExpansion {
        val assignments = combineAssignments((relevant map {
          (e) => e.getAssignmentsForTrue
        }): _*)

        def isConstant: Boolean = false

        def getConstantValue: Boolean = throw new AssertionError()

        def canAssignTrue: Boolean = true

        def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = assignments

        def canAssignFalse: Boolean = false

        def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = throw new AssertionError()
      }
    }
  }

  @throws(classOf[BoolExpansionAssignmentException])
  def disjunction(elems: BoolExpansion*): BoolExpansion = {
    for (elem <- elems)
      if (elem.isTrueConstant)
        return new ConstBoolExpansion(true)

    val relevant = elems filter {
      (elem) => !elem.isFalseConstant
    }

    if (relevant.length == 0)
      new ConstBoolExpansion(false)
    else if (relevant.length == 1)
      relevant.head
    else {
      /* We will only be able to assign false to this disjunction if we can
       * assign false to all it's values
       */
      for (e <- relevant)
        if (!e.canAssignFalse)
          throw new NoPossibleAssignmentsException


      new BoolExpansion {
        val assignments = combineAssignments((relevant map {
          (e) => e.getAssignmentsForFalse
        }): _*)

        def isConstant: Boolean = false

        def getConstantValue: Boolean = throw new AssertionError()

        def canAssignFalse: Boolean = true

        def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = assignments

        def canAssignTrue: Boolean = false

        def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = throw new AssertionError()
      }
    }
  }

  def negation(elem: BoolExpansion): BoolExpansion = {
    new BoolExpansion {
      def isConstant: Boolean = elem.isConstant

      def getConstantValue: Boolean = !elem.isConstant

      def canAssignFalse: Boolean = elem.canAssignTrue

      def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = elem.getAssignmentsForTrue

      def canAssignTrue: Boolean = elem.canAssignFalse

      def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = elem.getAssignmentsForFalse
    }
  }

  def comparison(variable: Variable, value: Literal[_]): BoolExpansion = {
    assert(variable.resultType == value.resultType)

    if (variable.resultType == Type.tBoolean) {
      new BoolExpansion {
        val vl: Boolean = value.asInstanceOf[Literal[Boolean]].value

        def canAssignFalse: Boolean = true

        def getConstantValue: Boolean = throw new AssertionError()

        def canAssignTrue: Boolean = true

        def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = Map((ResolvedVariable from variable) -> new Literal(vl))

        def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = Map((ResolvedVariable from variable) -> new Literal(!vl))

        def isConstant: Boolean = false
      }
    } else {
      new BoolExpansion {
        def isConstant: Boolean = false

        def getConstantValue: Boolean = throw new AssertionError()

        def canAssignFalse: Boolean = false

        def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = throw new AssertionError()

        def canAssignTrue: Boolean = true

        def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = Map((ResolvedVariable from variable) -> value)
      }
    }
  }

}

case class ConstBoolExpansion(value: Boolean) extends BoolExpansion {
  def isConstant: Boolean = true

  def getConstantValue: Boolean = value

  def canAssignTrue: Boolean = false

  def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = throw new AssertionError()

  def canAssignFalse: Boolean = false

  def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = throw new AssertionError()
}

/* Boolean Expressions
 * ~~~~~~~~~~~~~~~~~~~
 * A boolean expression is reversible (hence not read-only) if and only if ANY
 * of the following conditions hold:
 *
 * 1. It's defined simply as the value of a variable, where that variable is a
 *    free variable
 * 2. It's defined simply as the value of a variable, where that variable is
 *    defined with a reversible expression
 * 3. It's a comparison between a variable and a literal.
 *    In that case we only allow assignments of `true` into that expression
 *    (assignments of `false` will be ignored, and will log a warning)
 * 4. It's a conjunction of several expressions where all of them are either
 *    constant and evaluate to `true`, or simply reversible themselves.
 *    In that case we only allow assignments of `true` into that expression
 *    (assignments of `false` will be ignored, and will log a warning)
 * 5. It's a disjunction of several expressions where all of them are either
 *    constant and evaluate to `false`, or simply reversible themselves.
 *    In that case we only allow assignments of `false` into that expression
 *    (assignments of `true` will be ignored, and will log a warning)
 * 5. It's a negation of a reversible expression
 */
class BooleanExpressionExpander(precomp: SemanticAnalysis.WidgetAnalysis) extends ASTDeepVisitor {

  /**
   * This function tests whether an Boolean expression is reversible, and
   * expands it to a list of assignments needed to make it true/false (in cases
   * where it is possible). Its return value is determined according to the
   * following rules:
   *
   * - If a `true`/`false` value can be assigned into this expression, a
   *   `Some(BE:BooleanExpansion)` is returned describing the necessary
   *   assignments
   *
   * - Otherwise, `None` is returned
   */
  def expand(attr: Attribute): (Option[BoolExpansion], ReadOnlyStatus) = {
    assert(attr.getLeftType == Type.tBoolean)

    if (attr.isInstanceOf[InitialAttribute]) {
      (Some(new BoolExpansion {
        val astvar = ResolvedVariable from attr

        def canAssignFalse: Boolean = true

        def getConstantValue: Boolean = throw new AssertionError()

        def canAssignTrue: Boolean = true

        def getAssignmentsForTrue: Map[ResolvedVariable, Literal[_]] = Map(astvar -> new Literal(true))

        def getAssignmentsForFalse: Map[ResolvedVariable, Literal[_]] = Map(astvar -> new Literal(false))

        def isConstant: Boolean = false
      }), ReadOnlyStatus.ReadAndWrite)
    } else if (attr.isInstanceOf[ExpressionAttribute]) {
      val attrE = attr.asInstanceOf[ExpressionAttribute]
      val rv = ResolvedVariable from attrE

      /* First, test to see if it depends on conditionals or function calls */
      if (!((precomp.dependOnConditionals intersect (precomp.dependencies(rv) + rv)) isEmpty))
        return (None, ReadOnlyStatus.Conditional)
      if (!((precomp.dependOnFunctionCalls intersect (precomp.dependencies(rv) + rv)) isEmpty))
        return (None, ReadOnlyStatus.Functional)

      /* Otherwise, let's try to expand the expression! */
      try {
        val expr = expr2boolexp(attrE.realValue)
        if (expr.isConstant) {
          (Some(expr), ReadOnlyStatus.NothingToUpdate)
        } else {
          (Some(expr), ReadOnlyStatus.ReadAndWrite)
        }
      } catch {
        case ex: BoolExpansionAssignmentException =>
          (None, new ReadOnlyStatus(otherReversingError = Some(ex.getMessage)))
      }
    } else {
      /* This is the case where we have an attribute which is not an initial
       * attribute and not an attribute defined by an expression. This shouldn't
       * happen because we defined only these attribute classes!
       */
      throw new AssertionError()
    }
  }

  def expr2boolexp(expr: Expr): BoolExpansion = {
    (expr accept this).asInstanceOf[BoolExpansion]
  }

  /* The only way to introduce non boolean expressions would be through a
   * comparison, but we catch all of these in advance here! We don't go deep
   * into comparison nodes - we try the basic cases and then throw an error
   */
  override def visit(node: Comparision): BoolExpansion = {
    node match {
      case Comparision(variable:Variable, value:Literal[_]) => BoolExpansion.comparison(variable, value)
      case Comparision(value:Literal[_], variable:Variable) => BoolExpansion.comparison(variable, value)
      case Comparision(Literal(v1), Literal(v2)) => new ConstBoolExpansion(v1 == v2)
      case _ => throw new NonReversibleBooleanException
    }
  }

  override def visit(node: Disjunction): BoolExpansion = {
    BoolExpansion.disjunction(node.elems map {(e) => expr2boolexp(e)} : _*)
  }

  override def visit(node: Conjuction): BoolExpansion = {
    BoolExpansion.conjunction(node.elems map {(e) => expr2boolexp(e)} : _*)
  }

  override def visit[T](node: Literal[T]): BoolExpansion = {
    assert(node.resultType == Type.tBoolean) /* See comment above */
    new ConstBoolExpansion(node.asInstanceOf[Literal[Boolean]].value)
  }

  override def visit(node: Negation): BoolExpansion = {
    BoolExpansion.negation(expr2boolexp (node.expr))
  }

  override def visit(node: Variable): BoolExpansion = {
    assert(node.resultType == Type.tBoolean) /* See comment above */

    /* Now that we know this is a boolean variable, we can ask for an expansion
     * of it's definition as a BooleanExpansion object
     */
    precomp.booleanExpansions.get(ResolvedVariable from node) match {
      /* All the direct dependencies of this variable should have already been
       * analyzed, so we should have a value
       */
      case None => throw new AssertionError()
      /* Do we depend on a non reversible var? */
      case Some((None, _)) => throw new NonReversibleBooleanException

      case Some((Some(be), _)) => be
    }

  }

}
